In this paper, we formulate, analyze, and devise methodologies to verify the notion of infinite-step opacity in discrete event systems that are modeled as (possibly non-deterministic) finite automata with partial observation ...